%	This example of losing substitution for predicate parameters is essentially
% Carolyn's.  An axiom asserting the existence of two elements in the
% domain is added, and the schema is modified to be tautologous, so there
% can be no complaint about it.  I think the two element axiom is needed,
% the subsitution rule is probably correct in a one element domain.

DECLARE INDVAR r s t x;
DECLARE PREDCONST R 2;
DECLARE PREDPAR A 2;

declare INDCONST a b;

% Here come our two inoffensive axioms.

axiom twoelements:	¬(a=b);;
axiom lose: ∀r.(∃t.A(t,r) ⊃ ∃s.A(s,r));;

% Now the six commands.

∧i lose[A←λx s.¬(x=s)];
∀e ↑ b;
∃i twoelements a←t;
⊃e 3 2;
∃e ↑ x;
tauteq FALSE ↑;

% And here is the resulting proof.  Run the file to see it happen.

%1  ∀r.(∃t.¬(t=r)⊃∃s.¬(r=r))    ∧I lose
%2  ∃t.¬(t=b)⊃∃s.¬(b=b)    ∀E 1 b
%3  ∃t.¬(t=b)    ∃I twoelements a←t
%4  ∃s.¬(b=b)    ⊃E 3,2
%5  ¬(b=b)    ∃E 4 x
%6  FALSE    TAUTEQ FALSE 5